\begin{tabbing}
links2Fifo{-}impl(${\it es}$;$l_{1}$;$l_{2}$;$A$;${\it tg}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$<$$A$\+
\\[0ex], $A$
\\[0ex], \{$i$:Id$\mid$ ($i$ = source($l_{1}$)) $\vee$ ($i$ = destination($l_{1}$))\} 
\\[0ex], $\lambda$$i$,$j$,$e$. loc($e$) = $i$
\\[0ex]\& $\exists$${\it e'}$@$j$.((kind(${\it e'}$) = rcv($l_{1}$,${\it tg}$)) $\vee$ (kind(${\it e'}$) = rcv($l_{2}$,${\it tg}$))) \& sender(${\it e'}$) = $e$
\\[0ex], $\lambda$$i$,$e$. loc($e$) = $i$ \& ((kind($e$) = rcv($l_{1}$,${\it tg}$)) $\vee$ (kind($e$) = rcv($l_{2}$,${\it tg}$)))
\\[0ex], $\lambda$$i$,$x$,$y$. $x$ = $y$
\\[0ex], $\cdot>$
\-
\end{tabbing}